import Yices hiding (not)
import Data.List
import Control.Monad

-- Some custom types
type Binary = Nat -> Bool
data Piece = Piece
    { pRow :: Nat, pCol :: Nat
    , dR :: Nat, dC :: Nat
    }

-- Bits per ID
width = 3
rows  = 4
cols  = 5
board = liftM2 (,) [1..rows] [1..cols]

-- Board representation
s' :: Ident (Nat -> Nat -> Binary)
((s',s),(s0',s0),(s1',s1)) = decl ident3 "s"

decl :: (String -> a) -> String -> (a, a, a)
decl i n = (i n, i (n ++ "0"), i (n ++ "1"))

-- Binary representation of a number
infix 4 .=
(.=) :: (Nat -> Prop) -> Nat -> Prop
b .= n = conj $ zipWith beq (bits n) [b i | i <- [1..width]]
  where
    bits = unfoldr (Just . \x -> (odd x, x `div` 2))
    beq True  = id
    beq False = non

-- Successor arithmetic, tabular representation
follows :: (Nat -> Prop) -> (Nat -> Prop) -> Prop
x `follows` y = disj [ (x .= i+1) /\ (y .= i) | i <- [0..30]] 

-- Some initial positions
pieces :: [Piece]
pieces = config2
  where
    --    Piece row col dx dy
    config1 =
        [ Piece 3 2 1 2
        , Piece 1 3 1 3
        , Piece 1 1 3 1
        , Piece 2 4 2 1
        , Piece 3 5 2 1
        , Piece 4 1 1 2
        , Piece 4 3 1 2
        ]
    config2 =
        [ Piece 3 1 1 2
        , Piece 3 4 2 1
        , Piece 2 3 1 3
        , Piece 1 3 1 3
        , Piece 1 1 2 1
        ]

-- Construct the initial position
initial :: Prop
initial = conj $ map pieceAt board
  where
    pcs = zip [1..] pieces
    pieceAt (k,l) = case [ 
        n | (n, Piece i j di dj) <- pcs
        , k >= i && l >= j && k < i+di && l < j+dj
      ] of
        n:_ -> s k l .= n
        []  -> s k l .= 0

final :: Prop
final = conj [s 3 j .= 1 | j <- [cols-1,cols]]

trans :: Prop
trans = disj [availableMoves n | n <- [1,2]]

availableMoves :: Nat -> Prop
availableMoves n =
    disj    [move i j n   1   0 | i <- [2  ..rows-n], j <- [1  ..cols  ]]
    \/ disj [move i j n (-1)  0 | i <- [n+1..rows-1], j <- [1  ..cols  ]]
    \/ disj [move i j n   0   1 | i <- [1  ..rows  ], j <- [2  ..cols-n]]
    \/ disj [move i j n   0 (-1)| i <- [1  ..rows  ], j <- [n+1..cols-1]]

move :: Nat -> Nat -> Nat -> Nat -> Nat -> Prop
move i j n di dj =
    non (s0 i j .= 0)
    /\ conj [s0 i j == s0 (i+k*di) (j+k*dj) | k <- [1..n]]
    /\ s0 (i-di) (j-dj) .= 0
    /\ (if out (i+n*di+di) (j+n*dj+dj)
        then bool True
        else non (s0 i j == s0 (i+n*di+di) (j+n*dj+dj)))
    /\ conj [ s1 k l == s0 k l
        | (k,l) <- board
        , not (k Prelude.== i-di   && l Prelude.== j-dj  )
        , not (k Prelude.== i+n*di && l Prelude.== j+n*dj)
        ]
    /\ (s1 (i-di) (j-dj) == s0 i j)
    /\ (s1 (i+n*di) (j+n*dj) .= 0)
  where
    out  i j = i > rows || j > cols || i < 1 || j < 1
    x == y = conj [iff' ! x i ! y i | i <- [1..width]]

main = printBddReach initial trans final
